Skip to content

chore(Analysis/InnerProductSpace/Projection/Basic): remove an erw#38517

Open
yuanyi-350 wants to merge 2 commits intoleanprover-community:masterfrom
yuanyi-350:E_11
Open

chore(Analysis/InnerProductSpace/Projection/Basic): remove an erw#38517
yuanyi-350 wants to merge 2 commits intoleanprover-community:masterfrom
yuanyi-350:E_11

Conversation

@yuanyi-350
Copy link
Copy Markdown
Collaborator

@yuanyi-350 yuanyi-350 commented Apr 25, 2026

  • simplifies the inner-product rewrite chain to a plain simp, removing the erw

Extracted from #38415

Open in Gitpod

@yuanyi-350 yuanyi-350 added codex OpenAI Codex wrote (parts of) this PR. LLM-generated PRs with substantial input from LLMs - review accordingly labels Apr 25, 2026
@yuanyi-350 yuanyi-350 mentioned this pull request Apr 25, 2026
Open
18 tasks
@github-actions
Copy link
Copy Markdown

github-actions Bot commented Apr 25, 2026 •
edited
Loading

PR summary 36a97460d7

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows 
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

Decrease in tech debt: (relative, absolute) = (1.00, 0.00)
Current number Change Type
624 -1 erw

Current commit 43ca67bd7c
Reference commit 36a97460d7

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@github-actions github-actions Bot added the t-analysis Analysis (normed *, calculus) label Apr 25, 2026
themathqueen
themathqueen reviewed Apr 25, 2026
View reviewed changes
Comment thread Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean Outdated
@yuanyi-350 @themathqueen
Update Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean
43ca67b 
Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>
themathqueen
themathqueen approved these changes Apr 25, 2026
View reviewed changes
Copy link
Copy Markdown
Collaborator

@themathqueen themathqueen left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions Bot commented Apr 25, 2026

🚀 Pull request has been placed on the maintainer queue by themathqueen.

@mathlib-triage mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Apr 25, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@themathqueen themathqueen themathqueen approved these changes

Assignees

No one assigned

Labels

codex OpenAI Codex wrote (parts of) this PR. LLM-generated PRs with substantial input from LLMs - review accordingly maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-analysis Analysis (normed *, calculus)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@yuanyi-350 @themathqueen